\begin{tabbing}
w{-}machine{-}constraint($w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:Id.\+
\\[0ex]let ${\it Choose}$,${\it Trans}$,${\it Send}$ = w{-}machine($w$;$i$) in 
\\[0ex]$\forall$$t$:$\mathbb{N}$.
\\[0ex]($\neg$($\uparrow$isnull(a($i$;$t$))))
\\[0ex]$\Rightarrow$ \=(($\lambda$$x$.s($i$;$t$+1).$x$) = ($\lambda$$x$,$q$. ${\it Trans}$(kind(a($i$;$t$)),val(a($i$;$t$)),$\lambda$$x$.s($i$;$t$).$x$,$x$,$q$ + 1))\+
\\[0ex]\& (\=($\uparrow$islocal(kind(a($i$;$t$))))\+
\\[0ex]$\Rightarrow$ ($\exists$\=$x$:$\mathbb{N}$\+
\\[0ex](($\uparrow$isl(${\it Choose}$(act(kind(a($i$;$t$))),$x$,$\lambda$$x$.s($i$;$t$).$x$(0))))
\\[0ex]c$\wedge$ (val(a($i$;$t$)) = outl(${\it Choose}$(act(kind(a($i$;$t$))),$x$,$\lambda$$x$.s($i$;$t$).$x$(0)))))))
\-\-\\[0ex]\& m($i$;$t$) = ${\it Send}$(kind(a($i$;$t$)),val(a($i$;$t$)),$\lambda$$x$.s($i$;$t$).$x$(0)))
\-\-
\end{tabbing}